Nuprl Lemma : mk_lnk_wf
11,40
postcript
pdf
i
,
j
,
n
:Id. (link
n
from
i
to
j
)
IdLnk
latex
Definitions
Id
,
t
T
,
<
a
,
b
>
,
x
:
A
.
B
(
x
)
,
(link
n
from
i
to
j
)
,
IdLnk
Lemmas
Id
wf
origin
i, j, n:Id. (link n from i to j) 
IdLnk i, j, n:Id. (link n from i to j) IdLnk Tx:A. B(x)